(declare-fun v2 () Bool)
(declare-fun v5 () Bool)
(declare-fun v8 () Bool)
(declare-fun i1 () Int)
(declare-fun i2 () Int)
(declare-fun i6 () Int)
(declare-fun str4 () String)
(declare-fun str5 () String)
(declare-fun i7 () Int)
(assert v2)
(assert v5)
(assert (xor false false (distinct "t4" "" str5 (ite v8 "" (str.substr str4 (* i2 i7 i2 i6 i6) (div i6 (* i2 i7 i2 i6 i6)))) (str.substr str5 0 i1)) true false))
(check-sat)
